package kodkod.analysis;

import java.util.*;

import kodkod.analysis.ordering.*;
import kodkod.ast.*;
import kodkod.engine.config.AbstractReporter;
import kodkod.engine.config.Options;
import kodkod.engine.fol2sat.Skolemizer;
import kodkod.engine.fol2sat.Translation;
import kodkod.engine.fol2sat.Translator;
import kodkod.engine.fol2sat.TrivialFormulaException;
import kodkod.instance.Bounds;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.Simplifier;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;

public class Problem {
	public Module module;
	public Command command;
	
	TranslateAlloyToKodkod kodkod;
	
	Formula formula;
	public Bounds bounds;
	public Options options;
	
	public boolean satisfiable;
	
	public int nVars;
	public int nPrimaryVars;
	public int nClauses;
	
	public static int skolemDepth = 0;
	
	public Translation translation = null;
		
	public Problem(Module module, Command command) {
		this(module, command, null);
	}
	
	public Problem(Module module, Command command, AbstractOrdering ordering) {
		this.module = module;
		this.command = command;
		
		createKodkodTranslation();
		
		if (ordering != null) {
			this.translation = getTranslation(ordering);
		}
	}
	
	public Translation getTranslation(AbstractOrdering ordering) {
		try {
			options.ordering = ordering;
//			options.setSkolemDepth(skolemDepth);
			
			Translation translation = Translator.translate(formula, bounds, options);
		
			nVars = translation.cnf().numberOfVariables();
			nClauses = translation.cnf().numberOfClauses();
			nPrimaryVars = translation.numPrimaryVariables();
						
			return translation;
		} catch (TrivialFormulaException e) {
			e.printStackTrace();
			return null;
		}
	}

	public Formula getFormula() {
		return formula;
	}
	
	public Bounds getBounds() {
		return bounds;
	}
	
	public Options getOptions() {
		return options;
	}
		
	private void createKodkodTranslation() {
		try {
			A4Options options = new A4Options(A4Options.SatSolver.MiniSatJNI);
			options.skolemDepth = skolemDepth;
			kodkod = new TranslateAlloyToKodkod(A4Reporter.NOP, options, module.getAllReachableSigs(), command);
			kodkod.makeFacts(this.command.formula);
			
			if (kodkod.frame.formulas.size() > 0) {
				Simplifier simplifier = new Simplifier();
				if (!simplifier.simplify(A4Reporter.NOP, kodkod.frame, kodkod.frame.formulas)) {
					kodkod.frame.addFormula(Formula.FALSE, Pos.UNKNOWN);
				}				
				for (Relation r : kodkod.frame.bounds.relations()) {
					kodkod.frame.formulas.add(r.eq(r));
				}
			}
		} catch (Err e) {
			e.printStackTrace();
		}
		
		formula = Formula.and(kodkod.frame.formulas);
    	bounds = kodkod.frame.bounds;
    	options = kodkod.frame.solver.options();
	}
	
	public String getName() {
		String[] univ = module.getModelName().split("/");
    	return univ[univ.length-1] + "." + command.label;
	}
	
	public String toString() {
		String s = module.getModelName() + " " + command.label + " ";
		s += satisfiable ? "SAT" : "UNSAT";
		return s;
	}
}
